a:Id, T:Type, ds:x:Id fp Type, P:(State(ds)TProp), init:x:Id fp ds(x)?Void.
T
 AtomFree(Type;T)
 xdom(ds). A=ds(x)   A
 xdom(ds). A=ds(x)   AtomFree(Type;A)
 (s:State(ds). Dec(v:T. P(s,v)))
 Feasible(with ds: ds init: initaction a:T precondition a(v) is P) 

latex

Definitions

Type, Top, if b t else f fi, f(a), x:AB(x), x:A. B(x), x:A. B(x), A, P  Q, Dec(P), left+right, t  T, b, f(x), x  dom(f), xdom(f). v=f(x)   P(x;v), a:A fp B(a), P  Q, Knd, false, locl(a), KindDeq, eqof(d), p  q, Id, 1of(t), type List, IdDeq, deq-member(eq;x;L), AtomFree(T;x), IdLnk, False, State(ds), 2of(t), P & Q, (x  l), z != f(x)  P(a;z), M.sframe(k sends <l,tg>), M.frame(k affects x), f(x)?z, Feasible(M), mk-ma, , x : v, with ds: ds init: initaction a:T precondition a(v) is P, x. t(x), Prop, x:AB(x), Void, x.A(x), {x:A| B(x) }, x,y. t(x;y), True, true, b, p  q, , s = t, P  Q, P  Q, T, Unit, <a,b>

Lemmas

deq property, eqtt to assert, assert of bor, eqff to assert, squash wf, bnot thru bor, iff transitivity, assert of band, and functionality wrt iff, assert of bnot, bool wf, band wf, bnot wf, btrue wf, true wf, decidable wf, fpf-all wf, fpf-dom wf, fpf-trivial-subtype-top, atom-free wf, fpf-cap wf, fpf wf, ma-state wf, false wf, IdLnk wf, deq-member wf, id-deq wf, Id wf, assert wf, bor wf, eqof wf, Kind-deq wf, locl wf, bfalse wf, Knd wf, not wf